A, A':Type.
strong-subtype(A;A')
 (B:(AType), eq:EqDecider(A'), f, g:a:A fp B(a), x:A', P, Q:(a:AB(a)Prop).
 ((x:A, z:B(x). P(x,z)  Q(x,z))
 ( g  f
 ( (z != f(x)  P(x,z))
 ( (z != g(x)  Q(x,z))) 

latex

Definitions	(x  l), deq-member(eq;x;L), f(x), P  Q, P & Q, S  T, A & B, b, t  T, EqDecider(T), strong-subtype(A;B), Prop, x(s1,s2), x. t(x), z != f(x)  P(a;z), a:A fp B(a), x  dom(f), x:A. B(x), P  Q, f  g, x(s)
Lemmas	strong-subtype-deq-subtype, fpf-sub wf, fpf wf, deq wf, strong-subtype wf, strong-subtype-l member-type, assert-deq-member, deq-member wf, assert wf, l member wf